FDL - Nuprl Lemma : es-rcv-from-implies

Nuprl Lemma : es-rcv-from-implies

es:ES, e:E, l:IdLnk, L:E List.
rcvs from e on l = L

(

i:

||L||.

e':E. isrcv(e') & lnk(e') = l & sender(e') = e & index(e') = i

)

Definitions x:A. B(x), P Q, x:A. B(x), P & Q, t T, A & B, AB, A, False, Prop, rcvs from e on l = L, {i..j}, P Q, i j < k

Lemmas es-rcv-from-member-index, select wf, length wf1, select member, assert wf, es-isrcv wf, es-lnk wf, es-sender wf, es-index wf, int seg wf, es-Msgl wf, es-sends wf, es-E wf, es-rcv-from wf, IdLnk wf, event system wf